(set-logic QF_UF)
(declare-sort utt$8 0)
(declare-fun x () Bool)
(declare-fun z1 () utt$8)
(declare-fun z2 () utt$8)
(declare-fun y1 () utt$8)
(declare-fun y2 () utt$8)
(declare-fun n1 () utt$8)
(declare-fun n2 () utt$8)
(declare-fun n3 () utt$8)
(declare-fun s1 () utt$8)
(declare-fun s2 () utt$8)
(declare-fun s3 () utt$8)
(declare-fun s4 () utt$8)
(declare-fun s6 () utt$8)
(assert (= s2 (ite x n2 s1)))
(assert (= s3 (ite x n3 s1)))
(assert (= s4 s3))
(assert (= s6 s4))
(assert (= z2 s6))
(assert (= z1 z2))
(assert (= n1 z1))
(assert (distinct y1 n2 y2 n3 n1))
(check-sat)
(exit)
